Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Gabor/arity #4620

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Gabor/arity #4620

wants to merge 8 commits into from

Conversation

ggreif
Copy link
Contributor

@ggreif ggreif commented Jul 16, 2024

Note: a possibly wrong approach is in https://github.com/dfinity/motoko/tree/gabor/higher

but be sure to use the calling convention of the checker

right now the supertype is returned, though!
@ggreif ggreif self-assigned this Jul 16, 2024
(Nat, Nat) -> ((Nat, Nat))
cannot produce expected type
((Nat, Nat)) -> ((Nat, Nat))
issue-3318.mo:2.13-2.14: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test passes now, but should it? Needs thorough checking!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is issue #3318?

@@ -637,6 +637,11 @@ and check_typ' env typ : T.typ =
let c, typs2 = as_codomT sort.it typ2 in
let ts1 = List.map (check_typ env') typs1 in
let ts2 = List.map (check_typ env') typs2 in
if (typ.at.left.file = "Xstdin")
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

remove this debug code

let u, u' =
let open T in
if is_func t && is_func t' then
let transfer_arity from toh = match from, List.map normalize toh with
Copy link
Contributor Author

@ggreif ggreif Jul 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe we shouldn't normalise here, as it exposes (hidden) Tup, where none was before. We need the some tests, but also monomorphic ones to see if there are discrepancies.

@@ -73,34 +73,34 @@ to argument of type
<V>V -> V
to produce result of type
()
because no instantiation of T__102 makes
<V>V -> V <: <U>T__102 -> U
because no instantiation of T__105 makes
Copy link
Contributor Author

@ggreif ggreif Jul 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why did these numbers shift by 3?

| _, [Tup ts] -> ts
| _, _ -> toh in
let s, c, tbs, ts1, ts2 = as_func t in
let dom, cod = transfer_arity ts1, transfer_arity ts2 in
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Checking monomorphic lambdas uses as_domT/as_codomT, so maybe we should use it here too?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant